CSE 311: Homework 3 Part 1

Due: Tuesday, April 28th by 6:00 PM

Instructions

Complete the problems on the following pages.

Collaboration policy. You are required to submit your own solutions. You are allowed to discuss the homework with other students. However, you must complete the problems in Cozy on your own. Moreover, you must be able to explain your solution at any time. We reserve ourselves the right to ask you to explain your work at any time in the course of this class.

Late policy. You have a total of three late days during the quarter, but you can only use one late day on any one homework, giving an additional day on both parts. Please plan ahead.

Solutions submission. Submit your solution at http://cozy.cs.washington.edu

• Each part of each task is listed as its own problem.

• You have unlimited attempts on each part.

• All completed parts get full credit and uncompleted parts get no credit.

• Make sure that you understand each step that Cozy performs for you. In Part 2, you will not have Cozy’s help to make sure each step is performed correctly.

Task 1 – Cozy Congruence

For each of the following, write a formal inference proof in Cozy that the claim holds.

The allowed rules are Modus Ponens, Intro/Elim $\wedge$, Intro/Elim $\exists$, Intro/Elim $\forall$, Direct Proof, Algebra, and definitions of Divides and Congruent¹. Part (b) also allows the Cite and Apply rules for using theorems. No other rules are permitted.

1. Let $m$ be a positive integer. Given $a = b$, show that $a \equiv_m b$.

2. Let $a$ and $m$ be positive integers. Given that $\gcd(a, m) = 1$, show that $\exists x\, (a\,x \equiv_m 1)$.

   We proved this informally in class. You are asked to prove it formally.

   For this part, you may use the following theorem with the Cite or Apply rules²:

   Bézout’s Theorem $\forall u\, \forall v\, ((0 < u \wedge 0 < v) \to \exists s\, \exists t\, (s\,u + t\,v = \gcd(u, v)))$

Cozy’s documentation for inference proof problems is available here.

Task 2 – Cozy Modular Equation

Solve the following modular equation in Cozy: $$7x \equiv_{25} 4$$

Cozy’s documentation for modular equation problems is available here.

Task 3 – Cozy Induction

Write a formal inference proof in Cozy that the following claim holds for all integers $n\ge 0$. $$3 \mid (n^3 + 2n)$$

In addition to the rules allowed in Task 1, your proof should use the Induction rule. You can use this rule backward by just typing “induction” into the bottom box.

Hint. In the inductive step, you will want to expand $(k+1)^3 + 2(k+1)$ and rewrite it in a form that exposes a factor of $3$, using the inductive hypothesis to rewrite $k^3 + 2k$ as $3j$ for some integer $j$.